package bcontractor.base;

import bcontractor.api.SATReasoner;
import bcontractor.api.Sentence;
import bcontractor.api.SentenceSet;

/**
 * Abstract class to ease reasoner implementations.
 * 
 * @author lundberg
 * 
 */
public abstract class AbstractSATReasoner<S extends Sentence<S>> implements SATReasoner<S> {

    /**
     * {@inheritDoc}
     */
    @Override
    public boolean entails(SentenceSet<S> sentences, S sentence) {
        return this.isUnsatisfiable(sentences.with(sentence.negate()));
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public boolean isUnsatisfiable(SentenceSet<S> sentences) {
        return !this.isSatisfiable(sentences);
    }
}
